$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $P$:($A$$\rightarrow$Type$\rightarrow$Prop), $x$:$A$, $v$:Type.
\\[0ex]$\forall$$y$$\in$dom($x$ : $v$). $w$=$x$ : $v$($y$) $\Rightarrow$  $P$($y$,$w$) $\Leftrightarrow$ $P$($x$,$v$)